COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	February, 1982
C00011 ENDMK
C⊗;
February, 1982

The current version of our theorem-prover is available
on UTEXAS-20.  Although a number of changes have been made
since the user's manual (A Theorem-Prover for Recursive
Functions:  A Users' Manual, CSL-91, SRI International, on
line as AUX:<CL.TP2>CODE.DOC) was published two years ago, the user
interface is basically the same.

To run the theorem-prover, one should first exectute
the EXEC command

	@DEFINE DSK: DSK:, AUX:<CL.TP2>

rather than the command

	@DEFINE DSK: DSK:, <MOORE>.

Also, one should then say

	@RUN THM

rather than merely

	@THM.

Here are more of the most apparent changes to the user
interface.

(1) We have modified the formal theory.  A precise
description of the modifications may be found in Chapter III
of CSL report 108, "Metafunctions:  Proving them Correct and
Using Them Efficiently as New Proof Procedures."  CSL-108 is
misleading in one respect:  literal atom constants are
actually to be written in QUOTEs, e.g., (QUOTE ABC), instead
of with the quotation marks, e.g., "ABC", used in CSL-108.
[If you read all of CSL-108 you will appreciate why we lied
in there.]  In addition to the changes ennumerated in
CSL-108, certain additional functions are defined in the
initial BOOT.STRAP theory (e.g., TIMES, QUOTIENT, and
REMAINDER).  The variable BOOT.STRAP.INSTRS is a special
list of INTERLISP forms processed by BOOT.STRAP to "bring
up" the initial theory.  You are invited to inspect it as
temporary documentation of the theory.

(2) It is possible to run your defined functions on specific
data just as you might run lisp functions.  An exception is
any function defined in terms of a DCLd function -- e.g., one
for which no definition is available.  The new INTERLISP
routine R will evaluate a term composed entirely of runnable
functions and constants.  Thus, 

←R((PLUS 200 700))

produces 900.  In the above example, INTERLISP's "eval-quote"
typein mode was used.  R is in fact an INTERLISP lambda function.
Thus,

←(R (QUOTE (PLUS 200 700)))

produces 900.  [The QUOTE above is an INTERLISP quote to make R
get the right term when it evals its arg.]  If APPEND is defined 
as the usual function in our theory:

←R((APPEND (QUOTE (A B C)) (QUOTE (D E F))))

returns (QUOTE (A B C D E F)).  [In this example, the QUOTEs are
just abbreviations for CONS expressions in the theory.]

Formally, R returns the term that is the reduction of the given
reducible term (see pg 48 of CSL-108).  

R works by running compiled code for each function in the
given term.  If you would like to see the INTERLISP
expression compiled to define an INTERLISP routine for
computing the value of your function fn, call the routine
GET.INTERLISP.EXPR(fn).

(3) The META-lemma facility described in CSL-108 is
available.  To permit the system to use a user-defined
function, simp, as a new simplifier, cause the system to
PROVE.LEMMA a formula of the form *META on page 58 of
CSL-108.  As the list of lemma types (e.g., where you might
once have written (REWRITE)) you should write ((META foo)),
where foo is the name of a function symbol in your logic.
After *META is proved, the compiled version of simp will be
applied to every term of the form (foo ...) encountered by
the theorem-prover.  See CSL-108 for the details of the meta
facility.

(4) The arguments to ADD.SHELL have been changed.  See the
typical ADD.SHELL forms in BOOT.STRAP.INSTRS.

(5) The basic theorem-prover routine PROVE returns different
answers than before.  When the formula is proved it returns PROVED.
When a formula is not proved it returns NIL (not the failure message).
The routine PROVE.LEMMA returns either the name of the proved lemma
or NIL if it failed.

(6) The format of LIB files has changed.  Your old files are not
compatible with the new system.  

(7) It is more efficient to execute (INIT 'BOOT-STRAP.LIB)
than to execute (INIT T).

(8) When the theorem-prover creates a file on your directory (other
than a lib file created by your calling MAKE.LIB) it uses the
value of the variable MASTER.ROOT.NAME as the main name of the file
(or your login name if MASTER.ROOT.NAME is NIL).  Examples of
such files are .SWAPPED-LIB files created to gain space and the
.PROOF and .TTY files created by PROVEALL.  By setting MASTER.ROOT.NAME
appropriately you can have swapped lib files from several
different ongoing proof efforts on the same directory.  

(9) The new system creates a new temp file on your connected
directory named mst.EXPRS-SINCE-LAST-LIB, where mst is the
master root name as described above. This file contains the
INTERLISP translations of every function you have defined
since the last time you did a NOTE.LIB.  That information
must be kept around for the next MAKE.LIB to work and is
irrelevant thereafter.  Thus, if you NOTE.LIB(file), then do
some DEFNs etc, you will find an .EXPRS-SINCE-LAST-LIB on
your directory.  If you SYSOUT, you must have that same
.EXPRS-SINCE-LAST-LIB (and the same lib file) on your
directory when you next run that sysout.  If you eventually
make a new lib file with MAKE.LIB you can delete the
.EXPRS-SINCE-LAST-LIB file created before it because the
relevant information in it has been written to your new lib
file.

(10)  When an error occurs or you type CTRL-E, the system
prints ***ERROR*** on the tty.  This makes it easier (we find)
to look at dribble files of console sessions.

(11)  The function PUBLISH doesn't work very well in the new system.
Whether we will scrap it or fix it hasn't been determined.